perm filename SECOND.DOC[1,JRA]3 blob
sn#025631 filedate 1973-02-20 generic text, type T, neo UTF8
Preliminary User Manual February 20, 1973
Preliminary User's Manual for the Theorem Prover
The current program is a resolution- and paramodulation-based theorem
prover with extensive facilities for on-line control. Perhaps the
easiest introduction is to follow the development of a few examples.
Example 1.
Consider the following set of statements:
(1) (∀x∀y){P(x,y) ∧ P(y z) ⊃ G(x,z)}
(2) (∀y∃x){P(x,y)}
We might interpret these statements as claiming
"For all x and y, if x is the parent of y and y is the parent
of z, then x is the grandparent of z,"
and
"Everyone has a parent."
Given these statements as hypotheses we might wish to know if there
were individuals, x and y such that x is the grandparent of y. We
could pose that question as the statement:
(3) (∃x∃y){G(x,y)}
It is clear that (3) does indeed follow from (1) and (2). How do we
formulate the problem for the theorem prover?
Here is one axiomatization:
PRE_PRED: P,G;
VAR:x,y,z;
G1: ∀(x,y)(P(x,y) ∧ P(y,z) ⊃ G(x,z));
G2: ∀y∃x P(x,y);
THEOREM: ∃(x,y)G(x,y);
;
Some of the conventions displayed in the example are:
(1) the predicate letters and function symbols must be declared
according to their type. For example infix and prefix operators are
declared by INF_OP and PRE_OP respectively. Constants are considered
Preliminary User Manual February 20, 1973
to be prefix operators of zero arguments. (2) variables must be
declared;any extra variables which are needed in outputting derived
clauses are generated from the initial variable list. For example
x1,x2,...y1,y2... . (3) each statement must be terminated with a
semi-colon; (4) statements or sets of statements may be labeled.
These labels can by used to refer to clauses in the on-line editor.
If a statement is labeled, THEOREM, then the negation of that
statement is formed and is used in the list of input statements. (5)
adjacent like quantifiers may combined. (6) the whole set of
declarations and input statements must be delimited by a semicolon.
A complete description of the syntax and semantics of the input
format is given in the appendix.
Preliminary User Manual February 20, 1973
Example 2.
In an investigation of axiomatizations of elementary group theory the
following statements arose:
(1) x*x = y*y
(2) x*(y*y) = x
(3) x*(y*z) = z*(y*x)
(4) x*(x*y) = y
(5) (x*z)*(y*z) = x*y
Question: Does (5) follow from (1)-(4)?
The answer is "yes" but it is not immediately obvious. It is more
difficult to establish than Example 1. Notice that this Example is a
pure equality formulation, requiring only replacements of terms by
other terms. This example could be presented to the prover as:
INF_OP: *;
INF_PRED: =;EQUALITY:=;
VAR: x,y,z;
AXIOMS: x*x = y*y;
x*(y*y) = x;
x*(y*z) = z*(y*x);
x*(x*y) = y;
THEOREM:(x*z)*(y*z) = x*y;
;
In this example, the name AXIOMS, refers the first four statements.
Before presenting a more complicated example, we shall describe how
to use the prover on these first Examples.
Preliminary User Manual February 20, 1973
Once the input file has been prepared you are ready to used the
theorem prover. The command: RUN PROVER [P,JRA] , will select the
current version of the program. The appearence of an asterisk (*)
signifies that the program is ready. If you wish the program to make
an initial selection of strategies for your problem then type:
(PROVE DSK: filename). The exact strategies which are chosen are
described in Section ⊗⊗⊗. if you would rather select you own
strategies then type: (TRY DSK: filename). You will then be asked to
describe your choice and editing strategies. See Section ⊗⊗⊗ for a
complete description of strategy selection.
If the (translations of) the set of input statements are found to be
inconsistent, then the sequence of deductions which exhibits that
inconsistency is displayed on the console. This refutation and the
set of strategies which were employed are also saved on a disk file .
The name of the file is created from the name of the input file.
Thus, for example, (PROVE DSK: FOO) and (PROVE DSK: (FOO.A)) would
create an output file named #1FOO.PRF. If the input initially comes
for the console using (PROVE) or (TRY), then the output file is given
the name, #1PRF.PRF. It is also possible that the prover terminate
without finding a refutation. This could occur either because the
selected strategies do not form a complete set or because the initial
set is not inconsistent. In either case the program types NO-PROOF-
FOUND and enters the clause editor to wait for commands from the
user.
Preliminary User Manual February 20, 1973
Now let's try running the first example. Assume that a disk file,
EX1, has been prepared containing the axiomatization. What follows is
a running commentary on what should occur. Material preceeded by | is
commentary; statements typed by the user are preceeded by *.
*RUN PROVER [P,JRA] |retrieve the current prover.
*(PROVE DSK: EX1) |Request that the program pick the
|strategies while running EX1.
PRE_PRED: P,G; |The program is accepting the axioms.
VAR: x,y,z;
G1:
∀(x,y)(P(x,y) ∧ P(y,z)) ⊃ G(x,z));
G2:
∀y∃x P(x,y);
THEOREM:
∃(x,y)G(x,y);
HERE-ARE-THE-CLAUSES: |What follows are the translations
|of the input into clause-form, with
1 P(x,z)∧P(y,z) ⊃ G(x,y) |the redundant statements removed.
2 P(G21(x),x) |G21 is a generated Skolem function.
3 ¬G(x,y) |The translation of the negation of
|the theorem.
4 ¬(P(z,x)∧P(x,y)) |A deduction which has been added to
|the list of clauses.
COUNT = 1 |There was only one resolvent formed
LEVEL = 1 |on level one.
ELAPSED-TIME = 333 |The execution time in milliseconds.
5 ¬P(x,y);
COUNT = 3
LEVEL = 2 |Three resolvents have been formed by
ELAPSED-TIME = 500 |the end of level 2. (Two have been
|retained.)
NIL 1 4 |A contradiction. These next six
1 -P(x,y) 3 4 |lines are the refutation. I.e.:
3 ¬(P(z,x)∧P(x,y)) 5 6 | 6 5
4 P(G21(x),x) G2 | \ /
5 P(x,z)∧P(y,z) ⊃ G(x,y) G1 | 3 4
6 ¬G(x,y) THEOREM | \ /
| 1 4
| \ /
| NIL
Preliminary User Manual February 20, 1973
Notes:
1. The labeling of the input is reflected in the description
of the refutation tree. That is, P(G21(x),x) resulted from
the translation of G2; ¬G(x,y) came from the negation of the
theorem.
2. A copy of the refutation tree, relevant statistics, and a
description of the actual strategies used, now appears on a
file named #1EX1.PRF.
Preliminary User Manual February 20, 1973
Now let's run the second example. Assume that the axiomatization is
on a file named EX2.
*RUN PROVER [P,JRA]
*(PROVE DSK: EX2) |Again, let the program
|pick the strategies.
INF_OP: *;
INF_PRED: =;
EQUALITY: =;
VAR:x,y,z;
AXIOMS:
x*x=y*y;
x*(y*y)=x;
x*(y*z)=z*(y*x);
x*(x*y)=y;
THEOREM:
(x*z)*(y*z)=x*y;
HERE-ARE-THE-CLAUSES:
1 x*x=y*y
2 x*(y*y)=x
3 x*(y*z)=z*(y*x)
4 x*(x*y)=y
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2
|Again, THMn's are generated
|Skolem constants.
NIL 1 2 |An immediate contradiction
1 x=x; |We know E is reflexive
2 ¬THM1*THM2=THM1*THM2 3 4 |moderate mystery.
3 x*(y*z)=z*(y*x) AXIOMS
4 ¬(THM1*THM3)*(THM1*THM2)=THM1*THM2 THEOREM
Notes:
1. The `refutation' is a bit mysterious. A more sympathetic proof
recovery mechanism is contemplated, but perhaps some of the current
mystery can be dispelled.
A `natural' proof might be:
1. (x*z)*(y*z) = z*(y*(x*z)) replacement using (3)
2. z*(y*(x*z)) = z*(z*(x*y)) replacement using (3)
3. z*(z*(x*y)) = x*y replacement using (4)
Preliminary User Manual February 20, 1973
The above proof is indeed a translation of the machine proof.
Besides replacement, the prover also has a special rule of
simplification. Whenever an equality formulation is presented to the
prover, a list ,SL,is made consisting of all the equalities which
occur in the input. In the current example, SL would consist of
everything but the negation of the theorem. Let t1 = t2 be a member
of SL. Whenever a deduction is formed (but before it has been added
to the memory of the prover) we attempt to match t1 against terms
occurring in the deduction. If matches can be made we repalce those
terms with the appropriate instance of t2. It is this simplified
deduction which is presented to the prover.
Preliminary User Manual February 20, 1973
Thus the refutation really is:
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2 THEOREM
\
\
\ x*(y*z)=z*(y*x) AXIOMS
\ /
\ /
¬THM3*(THM2*(THM1*THM3))=THM1*THM2 by replacement
\
\
\ x*(y*z)=z*(y*x) AXIOMS
\ /
\ /
¬THM3*(THM3*(THM1*THM2))=THM1*THM2 by simplification
\
\
\ x*(x*y)=y AXIOMS
\ /
\ /
¬THM1*THM2=THM1*THM2 by simplification
\
\
\ x=x
\ /
\ /
NIL
by resolution
Preliminary User Manual February 20, 1973
Most applications of the prover lie in that gray area between a quick
proof and the occurrence of NO-PROOF. That is, an application of the
prover usually generated a large number of deductions before either a
proof is found or no more deductions can be made under the current
strategy settings. It is this area which can be profitably explored
using interactive commands. If the user sees a deduction which
should lead to the desired refutation he is able to guide the
program to the explicit contradiction. If he sees a deduction which
he feels is interesting, he can explore its consequences in the set
of statements. If he feels that the strategy settings are ill-chosen
then he can abort the current proof-search and pick new strategies.
The next sections give detailed descriptions of the current on-line
commands.
I. GENERAL BOOKEEPING COMMANDS.
CHange CH;
It is frequently desireable to change some of the
strategies while a proof attempt is in progress.
CHange describes what choice and editing strategies
are currently active and asks which are to be
changed.
CUrrent CU;
This command simply lists the current strategy
settings.
DSkout DS <filename>;
This command diverts future output to specified disk
file.
EVal EV;
Preliminary User Manual February 20, 1973
This command is mostly a debugging aid and is
included for completeness. The casual users should
not have to resort to its use. EVal enters a READ-
EVAL-PRINT. To return to the editor, type @END.
HAlt HA;
HAlt stops the prover is such a state that if the
current core image is saved, it can be continued. To
resume execution of such a core image, type RUN DSK:
name. When the asterisk appears you are in the on-
line editor. Then type TErminate.
End Of file EO;
EOf is used to terminate the DSkout command.
HElp HE;
This command will type a list of the available
editing commands along with an abbreviated
description of their action.
TErminate TE;
This command is used to terminate the editing process
and return to the prover.
Preliminary User Manual February 20, 1973
II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
Each clause which has been retained by the prover -- initial clauses
or deduction -- is given a number, the first axiom, the number 1.,
etc.. These numbers are permanently assigned, even though certain
actions of the prover may remove clauses from consideration by the
rules of inference. Clauses which have been so deleted are displayed
as *DE*. When the editor is entered, a hypothetical pointer is
initialized to the first clause. This first set of commands allow
the used to manipulate the set of clauses using the associated
numbers.
FLoat UP FU; or FL UP;
Moves the pointer up through the list of clauses.
The motion is stopped either by striking a key or by
reaching the upper extreme of the list. FLoat UP may
also be apbbreviated as FU.
FLoat DOwn FD; or FL DO;
The counterpart of FLoat UP. FLoat Down may also be
abbreviated as FD.
UP UP n;
UP is to be followed by an integer, N. The effect of
this command is to move the pointer up N clauses from
its current setting. As the pointer is moved, the
interviening clauses are printed. If N = 0, then the
pointer is immediately moved to the beginning of the
clause list. As with the FLoat commands,striking a
key will stop the pointer.
DOwn DO n;
The counterpart of UP. DOwn 0 moves the pointer to
the end of the list.
GO GO n;
Preliminary User Manual February 20, 1973
GO is to be followed by an integer designating a
clauses. The pointer goes immediately to the
designated clause.
Preliminary User Manual February 20, 1973
Though these commands have proved quite useful, experience has
shown that more global manipulation of the clauses is needed.
Therefore we have commands for assigning names to subsets of the
clause list, and commands for manipulating these sets. Just as each
element of the primary list of clauses is assigned a unique positive
integer, so is each element of each named subset. For example to
refer to the second element of the set named FOO, use FOO[2]; to
refer to the second and third elements, use FOO[2,3]. Certain
commands, like REsolve or PAramodualte create new names, like
RES1,RES2, etc. or PAR1, PAR2. These created names are local to that
call on the on-line editor. Names which were initiated by the user
using the SEt command are global.
The following BNF equations will be used in the sequel:
<clauses> ::= {<c>,}*<c>
<c> ::= <number>|<id>{[{<number>,}*<number>]}*
::= @<statment>|FIND[<id>;<pattern>]
CLear CL <id>;
CLear takes a name as argument. This command only
removes the name from the symbol table; it does not
affect the clauses attached to the name.
Delete DE <clauses>;
The designated clauses are deleted from the memory of
the prover. Attempts to display such clauses will
print *DE*. Other attempts to use deleted clauses in
editing commands will invoke an error message.
DIsplay DI <clauses>;
This command displays all the elements of <clauses>;_
Preliminary User Manual February 20, 1973
INsert IN <id> <statements>; IN <id> DSK: <file>;
This command is used to enter new clauses into the
clause editor. The first argument to INsert is a
<name>. What follows is a set of clauses, or a file
designator. If the clauses are typed they must
conform to the standard input format; if a file
designator is given, the specified file must be in
the correct format. IN is a special case of the SEt
command.
SAve SA <clauses>;
Most of the results of the on-line commands:
deductions, insertions, substitutions,etc, are local
to the clause editor. To include any of these
resulting clauses in the memory of the prover use the
Save command.
SEt SE <id> <clauses>;
SEt <id> <clauses>; has the effect of assigning to
<id>, the sequence of clauses selected by the
<clauses>. Within a particular proof attempt, the
names selected by the user are retained.
The commands listed above give us a reasonably powerful set of
instructions for manipulating the clause list. Clearly, before we can
really begin to guide the prover we must be able to perform the rules
of inference on-line. The next set of commands begins to do this.
III. COMMANDS FOR PERFORMING RULES OF INFERENCE
PAramodulate PA <clauses>; <clauses>;
This command handles equality replacements. All
equality literals of the form t1=t2, are used in
equality replacements in the following manner: let s
be any term, not a variable, which occurs in some
literal in one of the clauses. If s occurs no deeper
than PDEPTH (see the appendix for PDEPTH) and there
is a substitution unifying s and t1, then the
occurrence of t1 is replaced by the appropriate
instantiation of t2.
Preliminary User Manual February 20, 1973
REsolve RE <clauses>;<clauses>;
This command takes a pair of <clauses> as arguments.
The resolvents of these two sets are formed, a unique
name is generated and the resolvents are assigned to
that new name. The generated names are presently of
the form RESn, for some integer,n.
SImplify SImplify <clauses>; BY <clauses>;
This command is similar to the PA command. Here the
second set of clauses is to be a list of equality
units, again of the form t1=t2. Terms occuring in the
first set of clauses which unify with elements, t1,
are replaced by instances of t2. DDEPTH determines
the depth to which the match is attempted.
Example 3. A simple example of the use of the rules of inference.
Assume that R is the equality predicate and that we have just struck
a key on the console.
*DI 1,2,3; |Display the first three clauses
1 x≤y ⊃ x/y=0
2 ¬1/(a/b)=0
3 0≤x
*PA 1; 2; |Use replacement on 1 and 2.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME: PAR1 |PAR1 is a created name.
1 1≤a/b ⊃ 1=0
*PA 2; 3; |Try to use the replacement rule
NO-PARAMODULANTS |on clauses 2, and 3.
*RE 1; 3;
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:RES1 |RES1 is another created
|name.
1 0/x=0
*PA RES1; RES1; |Created names are legal.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:PAR2 |PAR2 is a new name.
1 0=0 |True.
Preliminary User Manual February 20, 1973
*SA PAR1[1]; |Add 1≤a/b ⊃ 1=0 to the memory
|of the prover;
Preliminary User Manual February 20, 1973
IV. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.
Though the commands, REsolve and PAramodulate, are useful for fine
control of the prover, is is often useful to demand larger inference
steps. That is, using some of the existing clauses in memory, with
perhaps some additional assumptions, we wish the prover to attempt to
establish the validity of a first order formula. While this subproof
is under investigation the state of the main proof should be
preserved. The commands in this section are used to initiate and
control such subproofs.
ABort AB ; or AB <clauses>;
This command is used to manually abort a proof
attempt, returning to the previous level. If
<clauses> is present, then the selected clauses are
returned and assigned to a created name.
USing US <clauses>; or US DSK: <file>;
The selected clauses are designated to be used in the
forthcoming subproof.
PRove PR <statement>; or PR DSK: <file>;
The <statement> is translated and will be attached to
the name LEMMA. The negation of the statement is also
formed and will be used in the subproof. Thus both
the positive and negative tanslates are formed. The
positive translate is maintained for the convenience
of the user since after the lemma has been
established it should be available for further
deductions. Within the subproof the negation of the
<statement> will appear under the local name, THMS.
These last two commands,--USing, and PRove -- are used to initialize
the call on the prover; USing may be omitted. There are two commands
to commence the subproof.
EXecute EX;
Preliminary User Manual February 20, 1973
EXecute begins the subproof using a computed set of
stategies.
TRy TR;
TRy first enters the strategy selection dialog, then
begins the subproof with the chosen strategies.
In both cases the strategies of the subproof are completely local.
They in no way affect the strategies in the parent proof. If a key is
struck while in the subproof the editor is entered and can manipulate
the local clauselist or initiate another subproof. The TErminate
command will comtinue the subproof, the ABort command will return to
the previous level.
Preliminary User Manual February 20, 1973
Example 3. A simple example of subproof generation.
Suppose that we have struck a key during a proof-search.
*AN 10; |Display the ancestry of
P(A) 1 2 |clause no. 10.
1 P(A) ∨ P(B) AX1
2 ¬P(B) HYP1
*USING 10, @P(A) ⊃ P(B); ; |Setup the assumptions for the
|lemma.
|Use clause no. 10 in the attempt
*PROVE @P(B);;
*EX; |This initiates the subproof.
NIL 1 2
1 P(A) DEDUCT |Clause 10 becomes an "axiom"
2 ¬P(A) 3 4 |with the subproof.
3 P(A)⊃P(B) INSERT
4 ¬P(B) THEOREM |The negation of the lemma
CONTRADICTION-FOUND-FOR-LEMMA
|We are now back in the editor
*DI 10; |Display clause no. 10.
P(A)
*DI LEMMA; |The translate of the statement
P(B) |to be PROVEed.
*USING LEMMA;
*PROVE @∃(x)P(x);; |LEMMA now becomes the translate
*EX; |this clause.
NIL 1 2
1 P(B) AX1
2 ¬P(X1) THEOREM
CONTRADICTION-FOUND-FOR-LEMMA
*DI LEMMA; |ED1 is a ubiquitous Skolem
P(ED1) |constant.
Preliminary User Manual February 20, 1973
V. COMMANDS USEFUL WHEN NO PROOF IS FOUND
When the prover is unable to make new deductions which satisfy the
current strategies it will report that no refutation can be found,
and will enter the on-line editor. At this time the user can examine
the list of clauses, perform rules of inference, initiate sub-proofs,
or use the other on-line commands. The user also has the opportunity
to save any or all of the current deductions and begin a the proof
search again, perhaps with new strategies. The user can also force a
proof attempt to be abandoned by typing AB;. This has exactly the
same effect as if the prover could make no new deductions.
ABandon AB;
AB, typed in this context (not in a subproof)
terminates the main proof attempt, enters the on-line
editor, and waits for commands.
TErminate TE <clauses>; or TE;
If <clauses> are present then they are added to the
list of clauses named THMS. The list, AXIOMS, HYPS,
and THMS are preserved and a new proof attempt is
begun. If the initial attempt was through PROVE then
the user is asked if he still wants automatic
strategy selection. If the initial attempt was
through TRY or the user does not wish automatic
selection, then a dialogue is begun describing the
current strategies and asking if changes are desired.
Then a new proof search is begun.
This use of AB and TE is useful for feeding `interesting' deductions
back into a proof search without having to restart the whole process.
The derivation tree of any such saved derived clause is maintained
for the proof recovery mechanisms but such clauses appear to be
`input' clauses to the rules of inference.